数学における証明と真理 第1部メモ
定義: 命題変項と論理式
加算無限個の命題変項の集合を$ \mathsf{Prop} := \{p,q,r,\dots\} 命題変項$ p
矛盾: $ \bot
論理式$ \varphi,\psiに対して$ \varphi \to \psi
論理式$ \varphiに対し$ \Box \varphi
省略
定義: 用語
Kripkeフレーム$ \mathcal{F} \coloneqq \lang W,R \rangと付値$ V : \mathsf{Prop} \to 2^Wに対し Kripkeモデル$ \mathcal{M} \coloneqq \lang \mathcal{F}, V \rangまたは$ \mathcal{M} \coloneqq \lang W,R, V \rangと表す． 論理式$ \varphiに対し
充足性$ \mathcal{M},w \models \varphi$ \iff$ \mathcal{M}の$ w \in Wで$ \varphiが真
モデル妥当性$ \mathcal{M} \models \varphi$ \iff任意の$ w \in Wで$ \mathcal{M},w \models \varphi
フレーム妥当性$ \mathcal{F} \models \varphi
$ \iff$ \mathcal{F}上の任意のモデル$ \mathcal{M}で$ \mathcal{M} \models \varphi
$ \iff$ \mathcal{F}上の任意の付値$ Vで$ \lang \mathcal{F},V \rang \models \varphi
フレームクラス妥当性$ \mathbb{F} \models \varphi$ \iff任意のフレーム$ \mathcal{F} \in \mathbb{F}で$ \mathcal{F} \models \varphi
論理式の集合$ \Gammaに対しても任意の$ \gamma \in \Gammaに対して成り立つという定義で定義できる．
充足性$ \mathcal{M},w \models \Gamma，
モデル妥当性$ \mathcal{M} \models \Gamma
フレーム妥当性$ \mathcal{F} \models \Gamma
フレームクラス妥当性$ \mathbb{F} \models \Gamma
定義: フレームクラスの定義
論理式の集合$ \Gammaがフレームクラス$ \mathbb{F}_\Gammaを定義するとは↓の同値が成り立つことである．
$ \mathcal{F} \in \mathbb{F_\Gamma} \iff \mathcal{F} \models \Gamma
特に$ \Gammaが単一要素の集合$ \Gamma = \{ \varphi \}であるとき，論理式$ \varphiがフレームクラス$ \mathbb{F}_\varphiを定義するともいう．
系
次の論理式は任意のフレームで成り立つわけではないが，成り立つとするとフレーム$ \mathcal{F}の到達可能性$ Rに制約がかかる．
$ \mathsf{T}: \Box p \to p，$ Rは反射律を満たす． $ \mathsf{B}: p \to \Box \Diamond p，$ Rは対称律を満たす $ \mathsf{4}: \Box \to \Box \Box p，$ Rは推移律を満たす． $ \mathsf{5}: \Diamond p \to \Box \Diamond p，$ RはEuclid的関係を満たす． $ \forall_{x,y,z}(xRy \& xRz \implies yRz)
$ \mathsf{D}: \Box p \to \Diamond p．$ Rは継起的 すなわち$ \forall_w \exists_v (wRv)
全ての$ wに関して何かしら$ wRvな$ vが存在する
$ \mathsf{.2}: \Diamond \Box p \to \Box \Diamond p，$ Rは有向的， すなわち$ \forall_{w,v,u}(wRv \& wRu \implies \exists_s(vRs \& uRs))
ダイアモンド型に閉じる．
$ \mathsf{L}: \Box(\Box p \to p) \to \Box p．$ Rは推移的かつ，$ R無限上昇列は存在しない．
フレーム$ \mathcal{F}に$ R無限上昇列が存在するとは，
$ \mathcal{F}の$ Wの中には無限列$ \{w_n\}_{n \in \omega}があって，任意の$ n \in \omegaに対し$ w_nR w_{n+1}が成り立つ．
すなわち，無限に遷移し続けられるような世界が存在することである
すなわち，次の論理式はフレームクラスを規定する．
$ \mathsf{T}はフレームクラス$ \mathbb{F}_\mathsf{T}を定理する．
証明は略．
定義: 命題変項への一様代入
命題記号$ p_1,\dots,p_nを適当な論理式に一斉に置き換える試みを命題記号への一様代入とよび，$ \sigma(\vec{p})として表す．
定義: 論理式への一様代入
論理式$ \varphiに対して帰納的に以下のように定める
$ \varphi \coloneqq pなら$ \bar{\sigma}(\varphi) = \sigma(p)
$ \varphi \coloneqq \botなら$ \sigma(\varphi) = \bot
$ \varphi \coloneqq \psi \to \chiなら$ \bar{\sigma}(\varphi) = \bar{\sigma}(\psi) \to \bar{\sigma}(\chi)
$ \varphi \coloneqq \Box \psiなら$ \bar{\sigma}(\varphi) = \Box \bar\sigma(\psi)
適当な論理式を代入した結果得られる論理式を代入例と呼ぶ．
次の公理と推論規則を持ったシステムは様相論理のHilbert流演繹体系$ \mathcal{H}_\mathsf{K}と言われる． 公理
$ \mathsf{Taut}: 命題論理のトートロジー
$ \mathsf{K}: $ \Box(p \to q) \to (\Box p \to \Box q)
推論規則
モーダス・ポネンスMP: $ \varphiと$ \varphi \to \psiから$ \psiを導いて良い． 必然化Nec: $ \varphiから$ \Box \varphiを導いて良い． 論理式への一様代入US : $ \varphiから$ \bar{\sigma}(\varphi)を導いて良い． 論理式の有限列$ \varphi_1,\dots,\varphi_nに対し，全ての$ \varphi_iについて↓が成り立つなら，$ \varphi_nは$ \mathcal{H}_\mathsf{K}の定理と$ \varphi_1,\dots,\varphi_nは$ \varphi_nの$ \mathcal{H}_\mathsf{K}での証明という．
$ \varphi_iが$ \mathcal{H}_\mathbf{K}の公理
$ j,k<iとし，$ \varphi_iが$ \varphi_j,\varphi_kからの$ \mathcal{H}_\mathbf{K}の推論規則で導かれる
例
$ \Box (\varphi \land \psi) \to \Box \varphiは$ \mathcal{H}_\mathbf{K}の定理であり，証明は以下．
1. $ p \land q \to p($ \mathsf{Taut})
2. $ \varphi \land \psi \to \varphi(1とUS)
3. $ \Box(\varphi \land \psi \to \varphi)(2とNec)
4. $ \Box(p \to q) \to (\Box p \to \Box q)($ \mathsf{K})
5. $ \Box((\varphi \land \psi) \to \varphi) \to (\Box (\varphi \land \psi) \to \Box \varphi)(4とUS)
6. $ \Box (\varphi \land \psi) \to \Box \varphi(3,5とMP)
定義: 正規様相論理
論理式の集合$ \Lambdaが正規様相論理(normal modal logic?)であるとき，次の2条件を満たす． $ \Lambdaは$ \mathcal{H}_\mathsf{K}の全ての公理を含んでいる．
$ \Lambdaは$ \mathcal{H}_\mathsf{K}の全ての推論規則に閉じている．
$ \Sigmaが論理式の集合であるとき，$ \Sigmaを含む最小の正規様相論理$ \mathbf{K\Sigma}とは以下で定義される．
$ \mathbf{K}\Sigma \coloneqq \bigcap \{ \Lambda: \text{normal modal logic} \mid \Sigma \sube \Lambda \}
$ \varphi \in \Lambdaを$ \vdash_\Lambda \varphiと書く．
系
次は一致する．論理式の集合$ \Sigmaに対して
$ \Sigmaを含む最小の正規様相論理$ \mathbf{K}\Sigma
$ \mathcal{H}_\mathsf{K}の公理に$ \Sigmaを付け加えて拡張した証明体系$ \mathcal{H}_{\mathsf{K}\Sigma}の定理の全体集合
例
$ \mathsf{Form}は$ \botを含む最小の正規様相論理である．
いくつかには別の名前がある
$ \mathbf{S4}とは$ \mathsf{T},\mathsf{4}を含む最小の正規様相論理$ \mathbf{KT4}のことである．様相論理S4 $ \mathbf{S5}とは$ \mathsf{T},\mathsf{5}を含む最小の正規様相論理$ \mathbf{KT5}のことである．様相論理S5 $ \mathbf{S4.2}とは$ \mathsf{T},\mathsf{4},\mathsf{.2}を含む最小の正規様相論理$ \mathbf{KT4.2}のことである．
$ \mathbf{GL}とは$ \mathsf{L}を含む最小の正規様相論理$ \mathbf{KL}のことである．様相論理GL $ \mathbf{S5}は$ \mathsf{T,B,4,5,D}の中での最小の様相論理の中では最強の論理である．
定義
正規様相論理$ \Lambdaがフレームクラス$ \mathbb{F}に対し健全
$ \iff$ \mathbb{F} \models \Lambda
$ \iff$ \vdash_\Lambda \varphi \implies \mathbb{F} \models \varphi
定理
任意の$ \Sigma \sube \{\mathsf{T,B,4,5,D,.2,L}\}について，$ \mathbf{K\Sigma}は$ \Sigmaが定義するフレームクラス$ \mathbb{F}_\Sigmaに対して健全である．
注意
$ \{\mathsf{T,L}\}が定義するフレームクラス$ \mathbb{F}_{\{\mathsf{T,L}\}}は空クラスである．
定理
任意の$ \Sigma \sube \{\mathsf{T,B,4,5,D,.2}\}について，$ \mathbf{K\Sigma}は無矛盾
すなわち，$ \not\vdash_\mathbf{K\Sigma} \bot
証明
健全性の対偶を示す．$ \mathbb{F}_{\Sigma} \not\models \botを示せば良い．
$ \mathbb{F}_{\Sigma} \not\models \bot$ \iff$ \mathbb{F}_{\Sigma} \not= \emptyset
SnO2WMaN.icon？
フレーム$ \mathcal{F} \coloneqq \lang \{ 0 \}, \{(0,0)\} \rangは$ \mathcal{F} \in \mathbb{F}_{\Sigma}
反射的，対称的，推移的，Eucid的，継起的．
系
その他の話題